Nuprl Lemma : mu-bound-unique
0,22
postcript
pdf
b
:
,
f
:(
b
),
x
:
b
.
f
(
x
) & (
y
:
b
.
f
(
y
)
y
=
x
)
mu(
f
) =
x
latex
Definitions
S
T
,
S
T
,
T
,
True
,
x
:
A
.
B
(
x
)
,
{
i
..
j
}
,
b
,
Prop
,
,
{
T
}
,
t
T
,
x
:
A
.
B
(
x
)
,
,
i
j
<
k
,
A
B
,
P
&
Q
,
A
,
False
,
P
Q
,
mu(
f
)
Lemmas
mu-bound-property
,
assert
wf
,
nat
wf
,
bool
wf
,
int
seg
wf
,
le
wf
,
mu
wf
,
mu-bound
origin
b:
, f:(b
), x:b. f(x) & (y:b. f(y) 
y = x 
) mu(f) = x b:, f:(b), x:b. f(x) & (y:b. f(y) y = x ) mu(f) = x 
T
T
T
x:A. B(x)
}
b Tx:A. B(x)
j < kB
A Q